$\forall$$b$:$\mathbb{N}$, $f$:(int\_seg(0; $b$)$\rightarrow\mathbb{B}$), $x$:int\_seg(0; $b$). \\[0ex](($\uparrow$($f$($x$))) $\wedge$ ($\forall$$y$:int\_seg(0; $b$). ($\uparrow$($f$($y$))) $\Rightarrow$ ($y$ = $x$ $\in$ $\mathbb{Z}$))) $\Rightarrow$ (mu($f$) = $x$ $\in$ $\mathbb{Z}$)